package fst.calculi.STLC

import fst.binding.Binding
import fst.parsing._


trait Parsing extends MoreCombinators with StdTokenParsers with ContextualParsers {
  val syntax: Syntax
  import syntax._
  
  type Lexical = StdLexical
  val lexical = new StdLexical
  lexical.delimiters += ("(", ")", ".", "=", "=>", "\\", ":")
  lexical.reserved += ("true", "false", "Bool")
  import lexical.EOF

  // Context tracks which variables are bound, the generic functionality is implemented in ContextualParsers
  // Here, we only specify how to create our Context class
  object Context extends ContextCompanion {
    def apply(f: String => Option[Name]): Context = new Context { def apply(n: String) = f(n) }
  }
  
  // since parsing a term depends on the variable bindings we have previously added to the context,
  // we put these parsers in a Context, which provides the `bind`, `in`, and `bound` combinators
  // these combinators take care of variable binding
  trait Context extends ContextCore {
    def term = chainl1(termSingle, success(App(_: Term, _: Term)))
    def termSingle: Parser[Term] = 
      ( "(" ~> term <~ ")"
      | ("\\" ~> bind(ident)) ~ (":" ~> typeP) >> {case cn ~ tp => in{ctx => "." ~> ctx.term}(cn) ^^ (Abs(tp, _))}
      | "true"                                            ^^ const(LTrue)
      | "false"                                           ^^ const(LFalse)
      | bound(ident)                                      ^^ Var
      )
      
    def typeSingle = ("(" ~> typeP <~ ")" | "Bool" ^^ const(TBool) )
    // TODO: intuitively, `=>` is right-associative (use chainr1)
    def typeP: Parser[Type] = chainl1(typeSingle, "=>" ^^ const(TArr(_: Type, _: Type))) 
  }
 
  def parse(input: String): Result[Term] = (Context.empty.term <~ EOF)(input) match {
    case ns: NoSuccess => bestNoSuccess getOrElse Failure("unknown failure!!", input)
    case s => s
  }
}

object ParsingTest extends Parsing {
  object syntax extends Syntax
  
  def main(args: Array[String]) = println(parse(args(0)))
}